(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_LRA)
(declare-fun v0 () Real)
(assert (let ((e1 1))
(let ((e2 (/ e1 e1)))
(let ((e3 (- e2)))
(let ((e4 (- v0 v0)))
(let ((e5 (> e2 e3)))
(let ((e6 (<= e2 e2)))
(let ((e7 (distinct e4 v0)))
(let ((e8 (ite e7 e3 v0)))
(let ((e9 (ite e7 e8 v0)))
(let ((e10 (ite e7 e8 v0)))
(let ((e11 (ite e5 e4 e2)))
(let ((e12 (ite e6 e2 e2)))
(let ((e13 (= e9 e2)))
(let ((e14 (< e11 e10)))
(let ((e15 (>= e4 e4)))
(let ((e16 (distinct e10 e9)))
(let ((e17 (<= e8 e11)))
(let ((e18 (>= e8 e8)))
(let ((e19 (<= e11 e4)))
(let ((e20 (<= e2 e12)))
(let ((e21 (distinct e2 e11)))
(let ((e22 (> e9 e11)))
(let ((e23 (<= e9 e4)))
(let ((e24 (= e2 e11)))
(let ((e25 (= e2 v0)))
(let ((e26 (> e9 e4)))
(let ((e27 (distinct e3 e9)))
(let ((e28 (not e20)))
(let ((e29 (xor e26 e5)))
(let ((e30 (= e6 e6)))
(let ((e31 (=> e22 e7)))
(let ((e32 (xor e21 e30)))
(let ((e33 (xor e19 e17)))
(let ((e34 (ite e27 e23 e18)))
(let ((e35 (not e24)))
(let ((e36 (or e34 e31)))
(let ((e37 (not e35)))
(let ((e38 (and e15 e16)))
(let ((e39 (not e32)))
(let ((e40 (=> e36 e28)))
(let ((e41 (or e33 e39)))
(let ((e42 (or e14 e41)))
(let ((e43 (= e37 e38)))
(let ((e44 (ite e25 e40 e25)))
(let ((e45 (or e43 e13)))
(let ((e46 (or e42 e45)))
(let ((e47 (= e29 e29)))
(let ((e48 (ite e47 e44 e44)))
(let ((e49 (= e48 e46)))
e49
))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
